Inference at * 
Iof proof for Lemma fseg weakening:


  T:Type, l1, l2:(T List). (l1 = l2)  fseg(T;l1;l2) 

latex

 by ((((Unfold `fseg` 0) 
CollapseTHEN (Auto'))) 
CollapseTHEN (((InstConcl [[]]) 

CoCollapseTHEN (Auto)))) 

latex

C1: 

C1: 1. T : Type
C1: 2. l1 : T List
C1: 3. l2 : T List
C1: 4. l1 = l2
C1:   l2 = ([] @ l1)
C.

Definitions	[], fseg(T;L1;L2), P  Q, x:A. B(x), x:A  B(x), Type, type List, , as @ bs, x:A. B(x), x:AB(x), s = t, t  T
Lemmas	append wf